; COMMAND-LINE: --decision=internal -q
; EXPECT: sat
(set-logic QF_SLIA)
(declare-const x Int)
(declare-fun s () String)
(declare-fun g () Int)
(assert (ite (str.prefixof "-" (str.substr s (+ 1 1) 1)) (and (distinct x (- 1)) (> (str.len (str.substr s 2 3)) 1)) (distinct (- 1) (str.to_int (str.substr s (+ 1 1) 1)))))
(assert (= 1 (str.len (str.substr s 1 1))))
(assert (= "0" (str.at (str.substr s 4 (- (str.len s) 4)) 0)))
(assert (< (ite (str.prefixof "-" (str.substr s 2 1)) (- (str.to_int (str.substr (str.substr s 2 g) 1 x))) (str.to_int (str.substr s (+ 1 1) (+ 1 1)))) 31))
(assert (ite (str.prefixof "-" (str.substr s 2 1)) (and (> (str.len (str.substr s 2 2)) 1) (distinct (- 1) (str.to_int (str.substr (str.substr s x x) 1 x)))) (distinct (- 1) (str.to_int (str.substr s (+ 1 1) (+ 1 1))))))
(assert (distinct "0" (str.substr s 2 1)))
(assert (= "0" (str.at (str.substr s 3 (- (str.len s) 3)) 0)))
(assert (distinct 1 (str.len (str.substr s (+ g 1) (- (str.len s) 1)))))
(assert (= 1 (str.len (str.substr s 2 1))))
(assert (= 1 (str.len (str.substr s 0 1))))
(assert (= 3 (- (str.len s) 1 1 1)))
(assert (str.in_re s (re.+ (re.range "0" "9"))))
(assert (< (ite (str.prefixof "-" (str.substr s 2 1)) (- (str.to_int (str.substr (str.substr s 2 2) 1 (- (str.len (str.substr s 2 (- g))) 1)))) (str.to_int (str.substr s 2 3))) 127))
(check-sat)
